\global\long\def\bef{\forwardcompose}%
\global\long\def\bbnum#1{\custombb{#1}}%


\chapter{Summary and problems}

\section{Exercises in applied functional type theory\label{chap:Exercises-in-AFTT}}

\subsection{Exercises}
\begin{enumerate}
\item Compute the smallest integer expressible as a sum of two cubed integers
in more than one way.
\item Read a text file, split it by spaces into words, and print the word
counts, sorted by decreasing count.
\item FPIS exercise 2.2: Check whether a sequence \lstinline!Seq[A]! is
sorted according to a given ordering function of type \lstinline!(A, A) => Boolean!.
\item FPIS exercise 3.24: Implement a function \lstinline!hasSubsequence!
that checks whether a \lstinline!List! contains another \lstinline!List!
as a subsequence. For instance, \lstinline!List(1,2,3,4)! would have
\lstinline!List(1,2)!, \lstinline!List(2,3)!, and \lstinline!List(4)!
as subsequences, among others. (Dynamic programming?)
\item The Seasoned Schemer, chapter 13: Implement \lstinline!remberUptoLast!
and \lstinline!remberBeyondLast!.
\begin{lstlisting}
def remberUptoLast[A](a: A, s: List[A]): List[A] = ???
def remberBeyondLast[A](a: A, s: List[A]): List[A] = ???

scala> remberUptoLast(4, List(1, 2, 3, 4, 5, 4, 5, 6, 7, 8))
List(5, 6, 7, 8)

scala> remberBeyondLast(4, List(1, 2, 3, 4, 5, 4, 5, 6, 7, 8))
List(1, 2, 3, 4, 5)
\end{lstlisting}
The function \lstinline!remberUptoLast! removes all elements from
a list up to and including the last occurrence of a given value. The
function \lstinline!remberBeyondLast! removes all elements from a
list starting from the last occurrence of a given value. Both functions
return the original list if the given value does not occur in the
list.
\item (Bird-de Moor, page 20) Derive the following identity between functions
$F^{A}\rightarrow F^{A}$, for any filterable functor $F$ and any
predicate $p^{:A\rightarrow\bbnum 2}$: 
\[
\text{filt}_{F}(p)=(\Delta\bef\text{id}\boxtimes p)^{\uparrow F}\bef\text{filt}_{F}(\pi_{2})\bef\pi_{1}^{\uparrow F}\quad.
\]
\item Define a monoid of partial functions with fixed types $P\rightarrow Q$.
\begin{lstlisting}
final case class PFM[P, Q](pf: PartialFunction[P, Q])
// After defining a monoid instance, the following code must work:
val p1 = PFM[Option[Int], String] { case Some(3) => "three" }
val p2 = PFM[Option[Int], String] {
  case Some(20)   => "twenty"
  case None       => "empty"
}
p1 |+| p2 // Must be the same as the concatenation of all `case` clauses.
\end{lstlisting}
\item Consider a typeclass called \textsf{``}\lstinline!Splittable!\textsf{''} for functors
$F^{\bullet}$ that have an additional method 
\[
\text{split}^{A,B}:F^{A+B}\rightarrow F^{A}+B
\]
with a non-degeneracy law
\[
(x^{:A}\rightarrow x+\bbnum 0^{:B})^{\uparrow F}\bef\text{split}=y^{:F^{A}}\rightarrow y+\bbnum 0^{:B}
\]
and a special associativity law for functions $F^{A+B+C}\rightarrow F^{A}+B+C$,
\[
\text{split}^{A+B,C}\bef\,\begin{array}{|c||cc|}
 & F^{A}+B & C\\
\hline F^{A+B} & \text{split}^{A,B} & \bbnum 0\\
C & \bbnum 0 & \text{id}
\end{array}\,=\text{split}^{A,B+C}\quad.
\]
Show that all polynomial functors $F^{\bullet}$ belong to this typeclass.
Show that exponential functors such as $F^{A}\triangleq Z\rightarrow A$
do not.
\item Given a monad $M$ and a fixed type $Z$, consider the functor $F^{A}\triangleq(A\rightarrow M^{Z})\rightarrow Z$.
Show that $F$ is a semimonad but not a full monad. Hint: use the
flipped Kleisli technique.
\item Given two fixed types $P$, $Q$ that are not known to be equivalent,
consider the contrafunctors $F^{A}\triangleq\left(\left(A\rightarrow P\right)\rightarrow P\right)\rightarrow Q$
and $G^{A}\triangleq A\rightarrow Q$. Show that there exist natural
transformations $F^{\bullet}\leadsto G^{\bullet}$ and $G^{\bullet}\leadsto F^{\bullet}$.
Show that these transformations are not isomorphisms.
\item Given two fixed types $P$, $Q$ that are not known to be equivalent,
show that the functor $L^{A}\triangleq\left(\left(\left(A\rightarrow P\right)\rightarrow Q\right)\rightarrow Q\right)\rightarrow P$
is a semimonad but not a full monad. (When $P\cong Q$, the functor
$L$ is also not a full monad because $L$ is then equivalent to a
composition of the continuation monad with itself. See Exercise~\ref{subsec:Exercise-monad-composition-mm}.)
\item When $M$ is a given semimonad, show that $M\circ M\circ...\circ M$
(with finitely many $M$) is also a lawful semimonad.
\end{enumerate}

\subsection{Open problems\index{problems}}

The author of this book does not know how to resolve these questions.

\subsubsection{Problem \label{par:Problem-monads}\ref{par:Problem-monads}}

Are there any polynomial monads not obtained by a chain of constructions
shown in Section~\ref{subsec:Constructions-of-polynomial-monads}?
The available constructions are:
\begin{itemize}
\item The polynomial monad $F^{A}\triangleq Z+W\times A$, where $W$ is
a monoid and $Z$ is a fixed type.
\item The free pointed monad $L^{A}\triangleq A+F^{A}$ where $F$ is a
monad.
\item The product monad $L^{A}\triangleq F^{A}\times G^{A}$ where $F$
and $G$ are monads.
\item The composed monad $L^{A}\triangleq F^{Z+W\times A}$ where $F$ is
a monad, $W$ is a monoid, and $Z$ is a fixed type.
\end{itemize}

\subsubsection{Problem \label{par:Problem-monads-1}\ref{par:Problem-monads-1}}

Do all polynomial functors of the form $P_{n}^{A}\triangleq\bbnum 1+\overbrace{A\times A\times...\times A}^{n\text{ times, }n\ge2}$
fail to be monads? An example is the functor $P_{2}^{A}\triangleq\bbnum 1+A\times A$,
which is not a monad because the monad laws are not satisfied by any
implementations of \lstinline!pure! and \lstinline!flatMap! methods
for that functor.\footnote{See discussion here: \texttt{\href{https://stackoverflow.com/questions/49742377}{https://stackoverflow.com/questions/49742377}}}

\subsubsection{Problem \label{par:Problem-monads-2}\ref{par:Problem-monads-2}}

Does a monad transformer exist for every monad whose \lstinline!pure!
and \lstinline!flatMap! methods are implemented using purely functional
code?

\subsubsection{Problem \label{par:Problem-monads-5-1}\ref{par:Problem-monads-5-1}}

We know that the monad transformers $T_{L}$ can be defined using
a \lstinline!swap! function for certain monads. Is this also the
case for any monad stacks built out of such monads? If each of the
monads $L_{1}$, $L_{2}$, ..., $L_{k}$ admits a transformer defined
via a lawful \lstinline!swap! function, will the monad $L_{1}\varangle L_{2}\varangle...\varangle L_{k}$
also admit a transformer with a \lstinline!swap! function? (See Section~\ref{subsec:Does-a-composition-have-swap}
for some results.)

\subsubsection{Problem \label{par:Problem-identity-natural-monad-morphism}\ref{par:Problem-identity-natural-monad-morphism}}

Are there any monadically natural monad morphisms $M\leadsto M$ that
are not identity? Equivalently, are there any natural transformations
$\text{Id}^{\bullet}\leadsto\text{Id}^{\bullet}$ between identity
functors in the category of monads, other than the identity transformation?

We look for a monad morphism $\varepsilon^{M,A}:M^{A}\rightarrow M^{A}$
that is defined for all monads $M$ and is monadically natural in
the parameter $M$. So, the function $\varepsilon$ must satisfy the
following laws:
\begin{align*}
{\color{greenunder}\text{naturality law}:}\quad & \varepsilon^{M,A}\bef(f^{:A\rightarrow B})^{\uparrow M}=(f^{:A\rightarrow B})^{\uparrow M}\bef\varepsilon^{M,B}\quad,\\
{\color{greenunder}\text{monad morphism laws}:}\quad & \text{pu}_{M}\bef\varepsilon=\text{pu}_{M}\quad,\quad\quad\varepsilon^{\uparrow M}\bef\varepsilon\bef\text{ftn}_{M}=\text{ftn}_{M}\bef\varepsilon\quad,\\
{\color{greenunder}\text{monadic naturality law}:}\quad & \varepsilon^{M,A}\bef\phi^{:M^{:A}\rightarrow N^{A}}=\phi^{:M^{A}\rightarrow N^{A}}\bef\varepsilon^{N,A}\quad,
\end{align*}
where $f^{:A\rightarrow B}$ is an arbitrary function, $M$, $N$
are arbitrary monads, and $\phi:M\leadsto N$ is an arbitrary monad
morphism. The problem is either to prove that any such $\varepsilon$
must be an identity function, $\varepsilon=\text{id}^{:M^{A}\rightarrow M^{A}}$,
or to show an example of such $\varepsilon$ not equal to identity.\footnote{See discussion here: \texttt{\href{https://stackoverflow.com/questions/61444425/}{https://stackoverflow.com/questions/61444425/}}}

If it were possible to show that any natural monad morphism $M\leadsto M$
is identity, there would be no need to verify the non-degeneracy law
for monad transformers\textsf{'} base runners.

\subsubsection{Problem \label{par:Problem-monads-3}\ref{par:Problem-monads-3}}

\textsf{``}Rigid functors\textsf{''} are defined in Section~\ref{subsec:Rigid-functors}.

\textbf{(a)} Are there any rigid functors that are not monads? 

\textbf{(b)} Are there any rigid functors that are not applicative?

\textbf{(c)} Is it true that any applicative rigid functor is a monad?

\subsubsection{Problem \label{par:Problem-monads-3-1}\ref{par:Problem-monads-3-1}}

Let $L$ be a fixed monad and $H$ be an $L$-filterable contrafunctor,
then the functor $F^{A}\triangleq H^{A}\rightarrow L^{A}$ is a lawful
monad (see Section~\ref{subsec:Constructions-of-M-filterables}).
What is a monad transformer for the monad $F$? 

Two nontrivial examples of $L$-filterable contrafunctors are $H^{A}\triangleq A\rightarrow L^{Z}$
and $H^{A}\triangleq L^{A}\rightarrow Z$ (where $Z$ is a fixed type).
For these cases, the monad transformers are defined by
\begin{align*}
 & \text{monad: }(A\rightarrow L^{Z})\rightarrow L^{A}\quad,\quad\quad\text{transformer: }(A\rightarrow T_{L}^{M,Z})\rightarrow T_{L}^{M,A}\quad,\\
 & \text{monad: }(L^{A}\rightarrow Z)\rightarrow L^{A}\quad,\quad\quad\text{transformer: }(T_{L}^{M,A}\rightarrow Z)\rightarrow T_{L}^{M,A}\quad,
\end{align*}
where $T_{L}^{M}$ is the monad $L$\textsf{'}s transformer applied to the
foreign monad $M$.

The problem is to implement the monad $F$\textsf{'}s transformer for an arbitrary
$L$-filterable contrafunctor $H$, and to prove that the transformer
laws hold.

\subsubsection{Problem \label{par:Problem-monads-5-2}\ref{par:Problem-monads-5-2}}

Assume an arbitrary unknown monad $M$ and define $L^{A}\triangleq\bbnum 1+A\times M^{L^{A}}$.
Can one define a lawful monad instance for the functor $L$? (This
is the \lstinline!List! monad\textsf{'}s transformer without the outer layer
of $M$. See Exercise~\ref{subsec:Exercise-effectful-list-not-monad}.)

\subsubsection{Problem \label{par:Problem-monads-5-2-1}\ref{par:Problem-monads-5-2-1}}

These questions concern the \lstinline!ListT! transformer: 
\[
T^{A}\triangleq M^{L^{A}}\quad,\quad\quad L^{A}\triangleq\bbnum 1+A\times M^{L^{A}}\quad,
\]
where $M$ is an arbitrary foreign monad. Normally, we cannot implement
fully parametric base runner $T^{A}\rightarrow M^{A}$ because we
cannot have a fully parametric runner $\text{List}^{A}\rightarrow A$
operating on arbitrary types $A$. However, for a monoid type $R$
with binary operation $\oplus_{R}$ and empty element $e_{R}$, the
type signature $\text{List}^{R}\rightarrow R$ is implemented by the
standard \lstinline!reduce! operation: 
\[
\text{reduce}:\text{List}^{R}\rightarrow R\quad,\quad\quad\text{reduce}\triangleq\,\begin{array}{|c||c|}
 & R\\
\hline \bbnum 1 & 1\rightarrow e_{R}\\
R\times\text{List}^{R} & h\times t\rightarrow h\oplus_{R}\overline{\text{reduce}}\,(t)
\end{array}\quad.
\]
We can similarly implement a base runner (\lstinline!brun!) for the
transformer $T_{\text{List}}$ if we restrict its usage to \emph{monoid}
types $R$. The function \lstinline!brun! with the type signature
$M^{L^{R}}\rightarrow M^{R}$ aggregates all elements of the effectful
list into a single value of type $M^{R}$ (which is also a monoid
type):
\[
\text{brun}:M^{L^{R}}\rightarrow M^{R}\quad,\quad\quad\text{brun}\triangleq\text{flm}_{M}\bigg(\,\begin{array}{|c||c|}
 & M^{R}\\
\hline \bbnum 1 & 1\rightarrow\text{pu}_{M}(e_{R})\\
R\times M^{L^{R}} & h\times t\rightarrow\text{pu}_{M}(h)\oplus_{M}\overline{\text{brun}}\,(t)
\end{array}\,\bigg)\quad.
\]
Here, we use the binary operation $\oplus_{M}$ of the monoid $M^{R}$,
defined by
\[
p^{:M^{R}}\oplus_{M}q^{:M^{R}}\triangleq p\triangleright\text{flm}_{M}\big(u^{:R}\rightarrow q\triangleright(v^{:R}\rightarrow u\oplus_{R}v)^{\uparrow M}\big)\quad.
\]

\textbf{(a)} Is \lstinline!brun! a monoid morphism $T^{A}\rightarrow A$?
(Note that $T^{A}$ is a monoid since $T$ is a lawful monad.)

\textbf{(b)} Do the monad morphism laws of \lstinline!brun! hold
when restricted to a monoid type $A$?
\begin{align*}
{\color{greenunder}\text{for all monoid types }A:}\quad & a^{:A}\triangleright\text{pu}_{T}\bef\text{brun}=a^{:A}\triangleright\text{pu}_{M}\quad,\\
{\color{greenunder}\text{composition law}:}\quad & p^{:T^{T^{A}}}\triangleright\text{ftn}_{T}\bef\text{brun }=p^{:T^{T^{A}}}\triangleright\text{brun}\bef\text{brun}^{\uparrow M}\bef\text{ftn}_{M}\quad.
\end{align*}
(If so, Exercise~\ref{subsec:Exercise-traversables-10-1} would show
that \lstinline!brun! is also a \emph{monoid} morphism $M^{L^{A}}\rightarrow M^{A}$.) 

The monoid morphism identity law holds for \lstinline!brun!. Does
the composition law hold?

\begin{comment}
Failed attempts to verify the composition law:

Write its two sides separately:
\begin{align*}
{\color{greenunder}\text{left-hand side}:}\quad & \text{ftn}_{T}\bef\text{brun}=\text{flm}_{M}(\text{prod})\bef\text{flm}_{M}\bigg(\,\begin{array}{||c|}
1\rightarrow\text{pu}_{M}(e_{R})\\
r\times t\rightarrow\text{pu}_{M}(r)\oplus_{M}\overline{\text{brun}}\,(t)
\end{array}\,\bigg)\\
{\color{greenunder}\text{associativity of }\text{flm}_{M}:}\quad & \quad=\text{flm}_{M}\bigg(\text{prod}\bef\text{flm}_{M}\bigg(\,\begin{array}{||c|}
1\rightarrow\text{pu}_{M}(e_{R})\\
r\times t\rightarrow\text{pu}_{M}(r)\oplus_{M}\overline{\text{brun}}\,(t)
\end{array}\,\bigg)\bigg)\quad,\\
{\color{greenunder}\text{right-hand side}:}\quad & \text{brun}^{T^{R}}\bef\text{brun}^{\uparrow M}\bef\text{ftn}_{M}=\text{flm}_{M}\bigg(\,\begin{array}{||c|}
1\rightarrow\text{pu}_{M}(e_{R})\\
r\times t\rightarrow\text{pu}_{M}(r)\oplus_{M^{T^{R}}}\overline{\text{brun}}{}^{T^{R}}(t)
\end{array}\,\bigg)\bef\text{flm}_{M}(\text{brun})\\
{\color{greenunder}\text{associativity of }\text{flm}_{M}:}\quad & \quad=\text{flm}_{M}\bigg(\,\begin{array}{||c|}
1\rightarrow\text{pu}_{M}(e_{T^{R}})\\
r\times t\rightarrow\text{pu}_{M}(r)\oplus_{M^{T^{R}}}\overline{\text{brun}}{}^{T^{R}}(t)
\end{array}\,\bef\text{flm}_{M}(\text{brun})\bigg)\quad.
\end{align*}
The remaining difference (under $\text{flm}_{M}$) is an equation
between functions of type $L^{M^{L^{R}}}\rightarrow M^{R}$:
\begin{align*}
 & \text{prod}\bef\text{flm}_{M}\bigg(\,\begin{array}{||c|}
1\rightarrow\text{pu}_{M}(e_{R})\\
r\times t\rightarrow\text{pu}_{M}(r)\oplus_{M}\overline{\text{brun}}\,(t)
\end{array}\,\bigg)=\text{prod}\bef\text{brun}\\
 & \quad\overset{?}{=}\,\begin{array}{||c|}
1\rightarrow\text{pu}_{M}(e_{T^{R}})\\
r^{:T^{R}}\times t^{:T^{T^{R}}}\rightarrow\text{pu}_{M}(r)\oplus_{M^{T^{R}}}\overline{\text{brun}}{}^{T^{R}}(t)
\end{array}\,\bef\text{flm}_{M}(\text{brun})\quad.
\end{align*}
It is inconvenient to use matrices at this step because the code of
$\text{flm}_{M}$ is unknown. Instead, we will substitute into both
sides an arbitrary value of type $L^{M^{L^{R}}}$, which can be one
of two possibilities, $\text{Nil}$ or $\bbnum 0+h^{:T^{R}}\times t^{T^{T^{R}}}$.
Substituting $\text{Nil}$, we get:
\begin{align*}
{\color{greenunder}\text{left-hand side}:}\quad & \gunderline{\text{Nil}\triangleright\text{prod}}\bef\text{brun}=\text{Nil}\triangleright\text{pu}_{M}\bef\text{brun}\\
{\color{greenunder}\text{use Eq.~(\ref{eq:listt-brun-derivation1})}:}\quad & \quad=e_{R}\triangleright\text{pu}_{M}\quad.\\
{\color{greenunder}\text{right-hand side}:}\quad & \text{Nil}\triangleright\,\begin{array}{||c|}
1\rightarrow\text{pu}_{M}(e_{T^{R}})\\
r\times t\rightarrow\text{pu}_{M}(r)\oplus_{M}\overline{\text{brun}}\,(t)
\end{array}\,\bef\text{flm}_{M}(\text{brun})\\
 & \quad=e_{T^{R}}\triangleright\gunderline{\text{pu}_{M}\triangleright\text{flm}_{M}}(\text{brun})=e_{R}\triangleright\gunderline{\text{pu}_{T}\bef\text{brun}}\\
{\color{greenunder}\text{identity law of }\text{brun}:}\quad & \quad=e_{R}\triangleright\text{pu}_{M}\quad.
\end{align*}
The two sides are now equal. It remains to substitute the second possibility:
\begin{align*}
{\color{greenunder}\text{left-hand side}:}\quad & (\bbnum 0+h\times t)\triangleright\text{prod}\bef\text{brun}=\\
 & \quad=(\bbnum 0+h\times t)\triangleright\,\begin{array}{||c|}
1\rightarrow\text{Nil}\triangleright\text{pu}_{M}\\
m\times p\rightarrow\text{comb}\,(m)(p\triangleright\text{flm}_{M}(\overline{\text{prod}})
\end{array}\bef\text{brun}\\
 & \quad=\big(\text{comb}\,(h)(t\triangleright\text{flm}_{M}(\overline{\text{prod}}))\big)\triangleright\text{brun}\\
 & \quad=h\triangleright\text{flm}_{M}\big(t\triangleright\text{flm}_{M}(\overline{\text{prod}})\triangleright\xi\big)\bef\text{flm}_{M}\bigg(\,\begin{array}{||c|}
1\rightarrow\text{pu}_{M}(e_{R})\\
r\times t\rightarrow\text{pu}_{M}(r)\oplus_{M}\overline{\text{brun}}\,(t)
\end{array}\,\bigg)\\
 & \quad=h\triangleright\text{flm}_{M}\big(t\triangleright\text{flm}_{M}(\overline{\text{prod}})\bef\xi\bef\text{brun}\big)\\
 & \quad=h\triangleright\text{flm}_{M}\big(t\triangleright\text{flm}_{M}(\overline{\text{prod}})\bef\big)\\
{\color{greenunder}\text{right-hand side}:}\quad & (\bbnum 0+h\times t)\triangleright\,\begin{array}{||c|}
1\rightarrow\text{pu}_{M}(e_{T^{R}})\\
h\times t\rightarrow\text{pu}_{M}(h)\oplus_{M}\overline{\text{brun}}\,(t)
\end{array}\,\bef\text{flm}_{M}(\text{brun})\\
 & \quad=(\text{pu}_{M}(h)\oplus_{M}\overline{\text{brun}}\,(t))\triangleright\text{flm}_{M}(\text{brun})\\
 & \quad=t\triangleright\overline{\text{brun}}\triangleright(v\rightarrow h\oplus_{R}v)^{\uparrow M}\triangleright\text{flm}_{M}(\text{brun})
\end{align*}
This is suspicious: we need to show that an expression $h\triangleright\text{flm}_{M}(t\triangleright...)$
is equal to $t\triangleright...$, and it seems impossible to convert
one into another, given that $h$ and $t$ are arbitrary values.

Note that
\[
\text{pu}_{M}(r^{:R})\oplus_{M}q^{:M^{R}}=r\triangleright\gunderline{\text{pu}_{M}\triangleright\text{flm}_{M}}(u\rightarrow q\triangleright(v\rightarrow u\oplus_{R}v)^{\uparrow M})=q\triangleright(v\rightarrow r\oplus_{R}v)^{\uparrow M}\quad.
\]
In particular,
\[
\text{pu}_{M}(p)\oplus_{M}\text{pu}_{M}(q)=q\triangleright\text{pu}_{M}\triangleright(v\rightarrow p\oplus_{R}v)^{\uparrow M}=q\triangleright(v\rightarrow p\oplus_{R}v)\triangleright\text{pu}_{M}=\text{pu}_{M}(p\oplus_{R}q)\quad.
\]
We also have the property of \lstinline!comb!:
\begin{align*}
 & \big(\text{comb}\,(p)(q)\big)\triangleright\text{flm}_{M}(g)=p\triangleright\text{flm}_{M}(q\triangleright\xi)\bef\text{flm}_{M}(g)=p\triangleright\text{flm}_{M}((q\triangleright\xi)\bef\text{flm}_{M}(g))\\
 & =p\triangleright\text{flm}_{M}\bigg(\begin{array}{||c|}
1\rightarrow q\\
h\times t\rightarrow\text{pu}_{M}\big(\bbnum 0+h\times\overline{\text{comb}}\,(t)(q)
\end{array}\,\bef\text{flm}_{M}(g)\bigg)
\end{align*}
\end{comment}

